es:ES, R:(EE).
(e, e':E. Dec(R(e',e)))
 R => x,y. (x < y)
 (e, e':E. (e' R e)  (es-r-immediate-pred(es;R;e';e))  (c:E. ((e' R c) & (c R e)))) 

latex

Definitions	x:A. B(x), E, (e < e'), P & Q, x f y, ES, , Type, R1 => R2, x. t(x), Dec(P), P  Q, left + right, es-r-immediate-pred(es;R;e';e), R!, x:A. B(x), A, False, P  Q, x:AB(x), Void, x:A  B(x), f(a), A c B, e < e', t.1, b, t  T
Lemmas	es-causl wf, decidable cand, decidable existse-causl